$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, ${\it eq}$:EqDecider($T$), $d$:$a$:$T$ fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$. non{-}void($d$) $\in$ Prop$_{\mbox{\scriptsize i'}}$